\functions {
int x0_0;
int x0;
int x0__0;
int x0_1;
int x0__1;
int x1;
int x1_0;
int x10;
int x10_0;
int x10__0;
int x10_1;
int x10__1;
int x11;
int x11_0;
int x11__0;
int x11_1;
int x11__1;
int x12;
int x12_0;
int x12__0;
int x12_1;
int x12__1;
int x13;
int x13_0;
int x13__0;
int x13_1;
int x13__1;
int x14;
int x14_0;
int x14__0;
int x14_1;
int x14__1;
int x15;
int x1__0;
int x1_1;
int x1__1;
int x2;
int x2_0;
int x2__0;
int x2_1;
int x2__1;
int x3;
int x3_0;
int x3__0;
int x3_1;
int x3__1;
int x4;
int x4_0;
int x4__0;
int x4_1;
int x4__1;
int x5;
int x5_0;
int x5__0;
int x5_1;
int x5__1;
int x6;
int x6_0;
int x6__0;
int x6_1;
int x6__1;
int x7;
int x7_0;
int x7__0;
int x7_1;
int x7__1;
int x8;
int x8_0;
int x8__0;
int x8_1;
int x8__1;
int x9;
int x9_0;
int x9__0;
int x9_1;
int x9__1;
}
\problem {
\part[left]((!(((((x0__1) - (x0__0))) >= (1))) | !(((((x0_0) - (x0))) >= (1)))) & (!(((((x1) - (x0__1))) >= (1))) | !(((((x0_0) - (x0))) >= (1)))) & (!(((((x0__0) - (x0))) >= (1))) | !(((((x0_1) - (x0_0))) >= (1)))) & (!(((((x0__1) - (x0__0))) >= (1))) | !(((((x0_1) - (x0_0))) >= (1)))) & (!(((((x1) - (x0__1))) >= (1))) | !(((((x0_1) - (x0_0))) >= (1)))) & (!(((((x0__0) - (x0))) >= (1))) | !(((((x1) - (x0_1))) >= (1)))) & (!(((((x0__1) - (x0__0))) >= (1))) | !(((((x1) - (x0_1))) >= (1)))) & (!(((((x1) - (x0__1))) >= (1))) | !(((((x1) - (x0_1))) >= (1)))) & (!(((((x1__0) - (x1))) >= (1))) | !(((((x1_0) - (x1))) >= (1)))) & (!(((((x1__1) - (x1__0))) >= (1))) | !(((((x1_0) - (x1))) >= (1)))) & (!(((((x2) - (x1__1))) >= (1))) | !(((((x1_0) - (x1))) >= (1)))) & (!(((((x1__0) - (x1))) >= (1))) | !(((((x1_1) - (x1_0))) >= (1)))) & (!(((((x1__1) - (x1__0))) >= (1))) | !(((((x1_1) - (x1_0))) >= (1)))) & (!(((((x2) - (x1__1))) >= (1))) | !(((((x1_1) - (x1_0))) >= (1)))) & (!(((((x1__0) - (x1))) >= (1))) | !(((((x2) - (x1_1))) >= (1)))) & (!(((((x1__1) - (x1__0))) >= (1))) | !(((((x2) - (x1_1))) >= (1)))) & (!(((((x2) - (x1__1))) >= (1))) | !(((((x2) - (x1_1))) >= (1)))) & (!(((((x2__0) - (x2))) >= (1))) | !(((((x2_0) - (x2))) >= (1)))) & (!(((((x2__1) - (x2__0))) >= (1))) | !(((((x2_0) - (x2))) >= (1)))) & (!(((((x3) - (x2__1))) >= (1))) | !(((((x2_0) - (x2))) >= (1)))) & (!(((((x2__0) - (x2))) >= (1))) | !(((((x2_1) - (x2_0))) >= (1)))) & (!(((((x2__1) - (x2__0))) >= (1))) | !(((((x2_1) - (x2_0))) >= (1)))) & (!(((((x3) - (x2__1))) >= (1))) | !(((((x2_1) - (x2_0))) >= (1)))) & (!(((((x2__0) - (x2))) >= (1))) | !(((((x3) - (x2_1))) >= (1)))) & (!(((((x2__1) - (x2__0))) >= (1))) | !(((((x3) - (x2_1))) >= (1)))) & (!(((((x3) - (x2__1))) >= (1))) | !(((((x3) - (x2_1))) >= (1)))) & (!(((((x3__0) - (x3))) >= (1))) | !(((((x3_0) - (x3))) >= (1)))) & (!(((((x3__1) - (x3__0))) >= (1))) | !(((((x3_0) - (x3))) >= (1)))) & (!(((((x4) - (x3__1))) >= (1))) | !(((((x3_0) - (x3))) >= (1)))) & (!(((((x3__0) - (x3))) >= (1))) | !(((((x3_1) - (x3_0))) >= (1)))) & (!(((((x3__1) - (x3__0))) >= (1))) | !(((((x3_1) - (x3_0))) >= (1)))) & (!(((((x4) - (x3__1))) >= (1))) | !(((((x3_1) - (x3_0))) >= (1)))) & (!(((((x3__0) - (x3))) >= (1))) | !(((((x4) - (x3_1))) >= (1)))) & (!(((((x3__1) - (x3__0))) >= (1))) | !(((((x4) - (x3_1))) >= (1)))) & (!(((((x4) - (x3__1))) >= (1))) | !(((((x4) - (x3_1))) >= (1)))) & (!(((((x4__0) - (x4))) >= (1))) | !(((((x4_0) - (x4))) >= (1)))) & (!(((((x4__1) - (x4__0))) >= (1))) | !(((((x4_0) - (x4))) >= (1)))) & (!(((((x5) - (x4__1))) >= (1))) | !(((((x4_0) - (x4))) >= (1)))) & (!(((((x4__0) - (x4))) >= (1))) | !(((((x4_1) - (x4_0))) >= (1)))) & (!(((((x4__1) - (x4__0))) >= (1))) | !(((((x4_1) - (x4_0))) >= (1)))) & (!(((((x5) - (x4__1))) >= (1))) | !(((((x4_1) - (x4_0))) >= (1)))) & (!(((((x4__0) - (x4))) >= (1))) | !(((((x5) - (x4_1))) >= (1)))) & (!(((((x4__1) - (x4__0))) >= (1))) | !(((((x5) - (x4_1))) >= (1)))) & (!(((((x5) - (x4__1))) >= (1))) | !(((((x5) - (x4_1))) >= (1)))) & (!(((((x5__0) - (x5))) >= (1))) | !(((((x5_0) - (x5))) >= (1)))) & (!(((((x5__1) - (x5__0))) >= (1))) | !(((((x5_0) - (x5))) >= (1)))) & (!(((((x6) - (x5__1))) >= (1))) | !(((((x5_0) - (x5))) >= (1)))) & (!(((((x5__0) - (x5))) >= (1))) | !(((((x5_1) - (x5_0))) >= (1)))) & (!(((((x5__1) - (x5__0))) >= (1))) | !(((((x5_1) - (x5_0))) >= (1)))) & (!(((((x6) - (x5__1))) >= (1))) | !(((((x5_1) - (x5_0))) >= (1)))) & (!(((((x5__0) - (x5))) >= (1))) | !(((((x6) - (x5_1))) >= (1)))) & (!(((((x5__1) - (x5__0))) >= (1))) | !(((((x6) - (x5_1))) >= (1)))) & (!(((((x6) - (x5__1))) >= (1))) | !(((((x6) - (x5_1))) >= (1)))) & (!(((((x6__0) - (x6))) >= (1))) | !(((((x6_0) - (x6))) >= (1)))) & (!(((((x6__1) - (x6__0))) >= (1))) | !(((((x6_0) - (x6))) >= (1)))) & (!(((((x7) - (x6__1))) >= (1))) | !(((((x6_0) - (x6))) >= (1)))) & (!(((((x6__0) - (x6))) >= (1))) | !(((((x6_1) - (x6_0))) >= (1)))) & (!(((((x6__1) - (x6__0))) >= (1))) | !(((((x6_1) - (x6_0))) >= (1)))) & (!(((((x7) - (x6__1))) >= (1))) | !(((((x6_1) - (x6_0))) >= (1)))) & (!(((((x6__0) - (x6))) >= (1))) | !(((((x7) - (x6_1))) >= (1)))) & (!(((((x6__1) - (x6__0))) >= (1))) | !(((((x7) - (x6_1))) >= (1)))) & (!(((((x7) - (x6__1))) >= (1))) | !(((((x7) - (x6_1))) >= (1)))) & (!(((((x7__0) - (x7))) >= (1))) | !(((((x7_0) - (x7))) >= (1)))) & (!(((((x7__1) - (x7__0))) >= (1))) | !(((((x7_0) - (x7))) >= (1)))) & (!(((((x8) - (x7__1))) >= (1))) | !(((((x7_0) - (x7))) >= (1)))) & (!(((((x7__0) - (x7))) >= (1))) | !(((((x7_1) - (x7_0))) >= (1)))) & (!(((((x7__1) - (x7__0))) >= (1))) | !(((((x7_1) - (x7_0))) >= (1)))) & (!(((((x8) - (x7__1))) >= (1))) | !(((((x7_1) - (x7_0))) >= (1)))) & (!(((((x7__0) - (x7))) >= (1))) | !(((((x8) - (x7_1))) >= (1)))) & (!(((((x7__1) - (x7__0))) >= (1))) | !(((((x8) - (x7_1))) >= (1)))) & (!(((((x8) - (x7__1))) >= (1))) | !(((((x8) - (x7_1))) >= (1)))) & (!(((((x8__0) - (x8))) >= (1))) | !(((((x8_0) - (x8))) >= (1)))) & (!(((((x8__1) - (x8__0))) >= (1))) | !(((((x8_0) - (x8))) >= (1)))) & (!(((((x9) - (x8__1))) >= (1))) | !(((((x8_0) - (x8))) >= (1)))) & (!(((((x8__0) - (x8))) >= (1))) | !(((((x8_1) - (x8_0))) >= (1)))) & (!(((((x8__1) - (x8__0))) >= (1))) | !(((((x8_1) - (x8_0))) >= (1)))) & (!(((((x9) - (x8__1))) >= (1))) | !(((((x8_1) - (x8_0))) >= (1)))) & (!(((((x8__0) - (x8))) >= (1))) | !(((((x9) - (x8_1))) >= (1)))) & (!(((((x8__1) - (x8__0))) >= (1))) | !(((((x9) - (x8_1))) >= (1)))) & (!(((((x9) - (x8__1))) >= (1))) | !(((((x9) - (x8_1))) >= (1)))) & (!(((((x9__0) - (x9))) >= (1))) | !(((((x9_0) - (x9))) >= (1)))) & (!(((((x9__1) - (x9__0))) >= (1))) | !(((((x9_0) - (x9))) >= (1)))) & (!(((((x10) - (x9__1))) >= (1))) | !(((((x9_0) - (x9))) >= (1)))))
 & 
\part[right]((!(((((x9__0) - (x9))) >= (1))) | !(((((x9_1) - (x9_0))) >= (1)))) & (!(((((x9__1) - (x9__0))) >= (1))) | !(((((x9_1) - (x9_0))) >= (1)))) & (!(((((x10) - (x9__1))) >= (1))) | !(((((x9_1) - (x9_0))) >= (1)))) & (!(((((x9__0) - (x9))) >= (1))) | !(((((x10) - (x9_1))) >= (1)))) & (!(((((x9__1) - (x9__0))) >= (1))) | !(((((x10) - (x9_1))) >= (1)))) & (!(((((x10) - (x9__1))) >= (1))) | !(((((x10) - (x9_1))) >= (1)))) & (!(((((x10__0) - (x10))) >= (1))) | !(((((x10_0) - (x10))) >= (1)))) & (!(((((x10__1) - (x10__0))) >= (1))) | !(((((x10_0) - (x10))) >= (1)))) & (!(((((x11) - (x10__1))) >= (1))) | !(((((x10_0) - (x10))) >= (1)))) & (!(((((x10__0) - (x10))) >= (1))) | !(((((x10_1) - (x10_0))) >= (1)))) & (!(((((x10__1) - (x10__0))) >= (1))) | !(((((x10_1) - (x10_0))) >= (1)))) & (!(((((x11) - (x10__1))) >= (1))) | !(((((x10_1) - (x10_0))) >= (1)))) & (!(((((x10__0) - (x10))) >= (1))) | !(((((x11) - (x10_1))) >= (1)))) & (!(((((x10__1) - (x10__0))) >= (1))) | !(((((x11) - (x10_1))) >= (1)))) & (!(((((x11) - (x10__1))) >= (1))) | !(((((x11) - (x10_1))) >= (1)))) & (!(((((x11__0) - (x11))) >= (1))) | !(((((x11_0) - (x11))) >= (1)))) & (!(((((x11__1) - (x11__0))) >= (1))) | !(((((x11_0) - (x11))) >= (1)))) & (!(((((x12) - (x11__1))) >= (1))) | !(((((x11_0) - (x11))) >= (1)))) & (!(((((x11__0) - (x11))) >= (1))) | !(((((x11_1) - (x11_0))) >= (1)))) & (!(((((x11__1) - (x11__0))) >= (1))) | !(((((x11_1) - (x11_0))) >= (1)))) & (!(((((x12) - (x11__1))) >= (1))) | !(((((x11_1) - (x11_0))) >= (1)))) & (!(((((x11__0) - (x11))) >= (1))) | !(((((x12) - (x11_1))) >= (1)))) & (!(((((x11__1) - (x11__0))) >= (1))) | !(((((x12) - (x11_1))) >= (1)))) & (!(((((x12) - (x11__1))) >= (1))) | !(((((x12) - (x11_1))) >= (1)))) & (!(((((x12__0) - (x12))) >= (1))) | !(((((x12_0) - (x12))) >= (1)))) & (!(((((x12__1) - (x12__0))) >= (1))) | !(((((x12_0) - (x12))) >= (1)))) & (!(((((x13) - (x12__1))) >= (1))) | !(((((x12_0) - (x12))) >= (1)))) & (!(((((x12__0) - (x12))) >= (1))) | !(((((x12_1) - (x12_0))) >= (1)))) & (!(((((x12__1) - (x12__0))) >= (1))) | !(((((x12_1) - (x12_0))) >= (1)))) & (!(((((x13) - (x12__1))) >= (1))) | !(((((x12_1) - (x12_0))) >= (1)))) & (!(((((x12__0) - (x12))) >= (1))) | !(((((x13) - (x12_1))) >= (1)))) & (!(((((x12__1) - (x12__0))) >= (1))) | !(((((x13) - (x12_1))) >= (1)))) & (!(((((x13) - (x12__1))) >= (1))) | !(((((x13) - (x12_1))) >= (1)))) & (!(((((x13__0) - (x13))) >= (1))) | !(((((x13_0) - (x13))) >= (1)))) & (!(((((x13__1) - (x13__0))) >= (1))) | !(((((x13_0) - (x13))) >= (1)))) & (!(((((x14) - (x13__1))) >= (1))) | !(((((x13_0) - (x13))) >= (1)))) & (!(((((x13__0) - (x13))) >= (1))) | !(((((x13_1) - (x13_0))) >= (1)))) & (!(((((x13__1) - (x13__0))) >= (1))) | !(((((x13_1) - (x13_0))) >= (1)))) & (!(((((x14) - (x13__1))) >= (1))) | !(((((x13_1) - (x13_0))) >= (1)))) & (!(((((x13__0) - (x13))) >= (1))) | !(((((x14) - (x13_1))) >= (1)))) & (!(((((x13__1) - (x13__0))) >= (1))) | !(((((x14) - (x13_1))) >= (1)))) & (!(((((x14) - (x13__1))) >= (1))) | !(((((x14) - (x13_1))) >= (1)))) & (!(((((x14__0) - (x14))) >= (1))) | !(((((x14_0) - (x14))) >= (1)))) & (!(((((x14__1) - (x14__0))) >= (1))) | !(((((x14_0) - (x14))) >= (1)))) & (!(((((x15) - (x14__1))) >= (1))) | !(((((x14_0) - (x14))) >= (1)))) & (!(((((x14__0) - (x14))) >= (1))) | !(((((x14_1) - (x14_0))) >= (1)))) & (!(((((x14__1) - (x14__0))) >= (1))) | !(((((x14_1) - (x14_0))) >= (1)))) & (!(((((x15) - (x14__1))) >= (1))) | !(((((x14_1) - (x14_0))) >= (1)))) & (!(((((x14__0) - (x14))) >= (1))) | !(((((x15) - (x14_1))) >= (1)))) & (!(((((x14__1) - (x14__0))) >= (1))) | !(((((x15) - (x14_1))) >= (1)))) & (!(((((x15) - (x14__1))) >= (1))) | !(((((x15) - (x14_1))) >= (1)))) & ((((x15) - (x0))) >= (1)) & (!(((((x0__0) - (x0))) >= (1))) | !(((((x0_0) - (x0))) >= (1)))))
 -> false
}
\interpolant{left; right}
